Nuprl Definition : mu
11,40
postcript
pdf
mu(
f
) == if
f
(0) then 0 else mu((
x
.
f
(
x
+ 1))) + 1 fi
(recursive)
latex
Definitions
Y
,
if
b
then
t
else
f
fi
FDL editor aliases
mu
origin
x.f(x + 1))) + 1 fi (recursive) x.f(x + 1))) + 1 fi (recursive)